\begin{tabbing}
E{-}State\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\{i\}\+
\\[0ex]$\times$ (${\it eq}$:EqDecider($E$)
\\[0ex]$\times$ ${\it pred?}$:($E$$\rightarrow$($E$ + Unit))
\\[0ex]$\times$ ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id)))
\\[0ex]$\times$ ${\it oaxioms}$:EO\=rderAxioms\{i\}($E$;\+
\\[0ex]${\it pred?}$;
\\[0ex]${\it info}$)
\-\\[0ex]$\times$ $T$:(Id$\rightarrow$Id$\rightarrow$Type\{i\})
\\[0ex]$\times$ $V$:(Id$\rightarrow$Id$\rightarrow$Type\{i\})
\\[0ex]$\times$ $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type\{i\})
\\[0ex]$\times$ ${\it init}$:($i$:Id$\rightarrow$EState($T$($i$)))
\\[0ex]$\times$ ${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$EState($T$($i$))$\rightarrow$EState($T$($i$)))
\\[0ex]$\times$ ${\it val}$:($e$:$E$$\rightarrow$kindcase(kind(${\it info}$;$e$); $a$.$V$(loc(${\it info}$;$e$),$a$); $l$,$t$.$M$($l$,$t$) ))
\\[0ex]$\times$ ${\it Send}$:\=($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$\+
\\[0ex](Msg($M$) List))
\-\\[0ex]$\times$ ${\it Choose}$:($i$:Id$\rightarrow$$a$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(($V$($i$,$a$)) + Unit))
\\[0ex]$\times$ ${\it time}$:($E$$\rightarrow\mathbb{Q}$)
\\[0ex]$\times$ (${\it va}$:\=val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;
\\[0ex]${\it Choose}$;${\it Send}$;${\it val}$;${\it time}$)
\-\\[0ex]$\times$ Top))
\-
\end{tabbing}